\section{Types}

\begin{quote}

\ntermdef{Type}

\defspace \keyw{void}

\defspace \opt{\keyw{callonce}} \nterm{LambdaStructure}

\defspace \opt{\nterm{Permission}} \nterm{NominalStructure}

\defspace (\nterm{Type})

\ntermdef{Permission}

\defspace \keyw{unique}

\defspace \nterm{SymmetricPermission}

\defspace \nterm{LocalPermission}

\ntermdef{SymmetricPermission}

\defspace \keyw{shared} <\nterm{SimpleExpr1}>

\defspace \keyw{immutable}

\ntermdef{LocalPermission} 

\defspace \keyw{local} \nterm{SymmetricPermission}

\ntermdef{LambdaStructure} 

\defspace \opt{\nterm{MetaParams}} (\nterm{ArgSpecs})
	-> \nterm{Type}

\ntermdef{NominalStructure} 

\defspace \keyw{top}

\defspace \nterm{QualifiedIdentifier} \opt{MetaArgs}

\ntermdef{ArgSpecs}

{\defspace \nterm{ArgSpec} \seq{ * \nterm{ArgSpec} }}
\end{quote}

All types in Plaid include a permission and a structure.  The most general
type is \keyw{void} which represents the weakest
permission, \keyw{none} (not otherwise expressible in the source), with the most 
general structure, \keyw{top}. References may be inferred to have the
type \keyw{dynamic}.  Uses of values with type \keyw{dynamic} are not statically
guaranteed to be type-safe.  An unsafe cast must appear in the source
for a \keyw{dynamic} value to be used in statically typed code. 
Lambda types consist of a lambda structure with an optional lambda permission 
\keyw{callonce}.  Normal functions can be called any number of times,
while a \keyw{callonce} function can only be called once.
All other types are written as an optional \nterm{Permission} and a structure.

A \nterm{LambdaStructure} represents a function structure.  
The environment included in the declaration of a lambda is
not included in its type.  However, if a function is specified to 
consume part of the permission to any of its environment variables, 
then it can only be typed at a \keyw{callonce}
lambda type since the necessary environment permission will no
longer be available after a call.  Consequently, once a 
\keyw{callonce} function has been called, its type becomes \keyw{void}.
Formally, a function that accepts multiple arguments actually accepts an
argument tuple, which is written with a \code{*}-separated list.

A \nterm{NominalStructure} represents the structure 
given by a declared state
or the distinguished \keyw{top} structure, which is a superstructure
of all structures.  If the state represented by the \nterm{NominalStructure}
is polymorphic, then \nterm{MetaArgs} must be provided.

If the permission for a nominal structure is not given, 
then a default is inferred.  The \keyw{top} structure 
defaults to the \keyw{none} permission.  A \nterm{NominalStructure} defaults 
to the default permission associated with the state it represents.

The \keyw{unique} permission indicates that there are no
usable aliases to the same object.  There may be other
references to the object with the \keyw{none} permission
which does not allow the object to be used in any way.

A \nterm{SymmetricPermission} allows new aliases to be 
created with the same permission.
\keyw{immutable} references cannot be used to update the object
but can assume that no other references make changes. 
\keyw{shared} references can make changes, but must assume that other
references may have changed the object.

A \keyw{local} permission gives the same abilities
and guarantees as its underlying \nterm{SymmetricPermission}, 
but is restricted to local variables and parameters.  
A \keyw{local} reference cannot be assigned into a field.
This restriction allows \keyw{local} permissions to be
returned to their original location when their reference goes out of 
scope.  This may allow the original reference to regain a stronger permission.
For example, a \keyw{unique} reference used as a function parameter
that requires and results in a \keyw{local} permission will
still be \keyw{unique} after the function call.  Refer to \cite{naden12:borrowingPermissions}
for more information on \keyw{local} permissions.

